Владимир Анатольевич Захаров (zakh@cs.msu.su)
Владислав Васильевич Подымов (valdus@yandex.ru)

Будет как теория, так и практика.
Курс в целом - математический.

Сайт курса:
    http://mk.cs.msu.ru/index.php/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B8%D0%B5_%D0%BC%D0%B5%D1%82%D0%BE%D0%B4%D1%8B_%D0%B2%D0%B5%D1%80%D0%B8%D1%84%D0%B8%D0%BA%D0%B0%D1%86%D0%B8%D0%B8_%D1%81%D1%85%D0%B5%D0%BC_%D0%B8_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC


Экзамен - в письменной форме из 3-х частей:

1) 3 задачи по 3-м темам, на которые были семинары:
    1.1) построить темпоральные формулы для задания свойств поведения
    1.2) явная работа (таличная работа) алгоритмов верификации - проверка выполнимости формул логики CTL - деревьев вычислений на конечной модели
    1.3) задача на демонстрацию того, что мы понимаем, как происходит преобразование двоичной разрешающей диаграммы, т.е. построение ROBDD по булевой формуле (формула с 3-4 переменными)
2) потом будет 4 вопроса на знание определений и понятий, формулировок, ключевых утверждений, описания содержания ключевых алгоритмов и методов
3) 2-3 вопроса, которые потребуют некоторых рассуждений - нужно будет выбрать и обосновать правильные варианты ответа

Билеты - это темы занятий (написаны на слайдах).
Пользоваться нельзя НИЧЕМ.